Left Termination of the query pattern
sublist(g,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 88 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 41 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇒, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES

(0) Obligation:

Clauses:

append1([], Ys, Ys).
append1(.(X, Xs), Ys, .(X, Zs)) :- append1(Xs, Ys, Zs).
append2([], Ys, Ys).
append2(.(X, Xs), Ys, .(X, Zs)) :- append2(Xs, Ys, Zs).
sublist(X, Y) :- ','(append1(P, X1, Y), append2(X2, X, P)).

Query: sublist(g,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

append1A(.(X1, X2), X3, .(X1, X4)) :- append1A(X2, X3, X4).
append2B(.(X1, X2), X3, .(X1, X4)) :- append2B(X2, X3, X4).
sublistC(X1, .(X2, X3)) :- append1A(X4, X5, X3).
sublistC(X1, .(X2, X3)) :- ','(append1cA(X4, X5, X3), append2B(X6, X1, X4)).

Clauses:

append1cA([], X1, X1).
append1cA(.(X1, X2), X3, .(X1, X4)) :- append1cA(X2, X3, X4).
append2cB([], X1, X1).
append2cB(.(X1, X2), X3, .(X1, X4)) :- append2cB(X2, X3, X4).

Afs:

sublistC(x1, x2)  =  sublistC(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
sublistC_in: (b,b)
append1A_in: (f,f,b)
append1cA_in: (f,f,b)
append2B_in: (f,b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

SUBLISTC_IN_GG(X1, .(X2, X3)) → U3_GG(X1, X2, X3, append1A_in_aag(X4, X5, X3))
SUBLISTC_IN_GG(X1, .(X2, X3)) → APPEND1A_IN_AAG(X4, X5, X3)
APPEND1A_IN_AAG(.(X1, X2), X3, .(X1, X4)) → U1_AAG(X1, X2, X3, X4, append1A_in_aag(X2, X3, X4))
APPEND1A_IN_AAG(.(X1, X2), X3, .(X1, X4)) → APPEND1A_IN_AAG(X2, X3, X4)
SUBLISTC_IN_GG(X1, .(X2, X3)) → U4_GG(X1, X2, X3, append1cA_in_aag(X4, X5, X3))
U4_GG(X1, X2, X3, append1cA_out_aag(X4, X5, X3)) → U5_GG(X1, X2, X3, append2B_in_agg(X6, X1, X4))
U4_GG(X1, X2, X3, append1cA_out_aag(X4, X5, X3)) → APPEND2B_IN_AGG(X6, X1, X4)
APPEND2B_IN_AGG(.(X1, X2), X3, .(X1, X4)) → U2_AGG(X1, X2, X3, X4, append2B_in_agg(X2, X3, X4))
APPEND2B_IN_AGG(.(X1, X2), X3, .(X1, X4)) → APPEND2B_IN_AGG(X2, X3, X4)

The TRS R consists of the following rules:

append1cA_in_aag([], X1, X1) → append1cA_out_aag([], X1, X1)
append1cA_in_aag(.(X1, X2), X3, .(X1, X4)) → U7_aag(X1, X2, X3, X4, append1cA_in_aag(X2, X3, X4))
U7_aag(X1, X2, X3, X4, append1cA_out_aag(X2, X3, X4)) → append1cA_out_aag(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append1A_in_aag(x1, x2, x3)  =  append1A_in_aag(x3)
append1cA_in_aag(x1, x2, x3)  =  append1cA_in_aag(x3)
append1cA_out_aag(x1, x2, x3)  =  append1cA_out_aag(x1, x2, x3)
U7_aag(x1, x2, x3, x4, x5)  =  U7_aag(x1, x4, x5)
append2B_in_agg(x1, x2, x3)  =  append2B_in_agg(x2, x3)
SUBLISTC_IN_GG(x1, x2)  =  SUBLISTC_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x1, x2, x3, x4)
APPEND1A_IN_AAG(x1, x2, x3)  =  APPEND1A_IN_AAG(x3)
U1_AAG(x1, x2, x3, x4, x5)  =  U1_AAG(x1, x4, x5)
U4_GG(x1, x2, x3, x4)  =  U4_GG(x1, x2, x3, x4)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x1, x2, x3, x4)
APPEND2B_IN_AGG(x1, x2, x3)  =  APPEND2B_IN_AGG(x2, x3)
U2_AGG(x1, x2, x3, x4, x5)  =  U2_AGG(x1, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUBLISTC_IN_GG(X1, .(X2, X3)) → U3_GG(X1, X2, X3, append1A_in_aag(X4, X5, X3))
SUBLISTC_IN_GG(X1, .(X2, X3)) → APPEND1A_IN_AAG(X4, X5, X3)
APPEND1A_IN_AAG(.(X1, X2), X3, .(X1, X4)) → U1_AAG(X1, X2, X3, X4, append1A_in_aag(X2, X3, X4))
APPEND1A_IN_AAG(.(X1, X2), X3, .(X1, X4)) → APPEND1A_IN_AAG(X2, X3, X4)
SUBLISTC_IN_GG(X1, .(X2, X3)) → U4_GG(X1, X2, X3, append1cA_in_aag(X4, X5, X3))
U4_GG(X1, X2, X3, append1cA_out_aag(X4, X5, X3)) → U5_GG(X1, X2, X3, append2B_in_agg(X6, X1, X4))
U4_GG(X1, X2, X3, append1cA_out_aag(X4, X5, X3)) → APPEND2B_IN_AGG(X6, X1, X4)
APPEND2B_IN_AGG(.(X1, X2), X3, .(X1, X4)) → U2_AGG(X1, X2, X3, X4, append2B_in_agg(X2, X3, X4))
APPEND2B_IN_AGG(.(X1, X2), X3, .(X1, X4)) → APPEND2B_IN_AGG(X2, X3, X4)

The TRS R consists of the following rules:

append1cA_in_aag([], X1, X1) → append1cA_out_aag([], X1, X1)
append1cA_in_aag(.(X1, X2), X3, .(X1, X4)) → U7_aag(X1, X2, X3, X4, append1cA_in_aag(X2, X3, X4))
U7_aag(X1, X2, X3, X4, append1cA_out_aag(X2, X3, X4)) → append1cA_out_aag(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append1A_in_aag(x1, x2, x3)  =  append1A_in_aag(x3)
append1cA_in_aag(x1, x2, x3)  =  append1cA_in_aag(x3)
append1cA_out_aag(x1, x2, x3)  =  append1cA_out_aag(x1, x2, x3)
U7_aag(x1, x2, x3, x4, x5)  =  U7_aag(x1, x4, x5)
append2B_in_agg(x1, x2, x3)  =  append2B_in_agg(x2, x3)
SUBLISTC_IN_GG(x1, x2)  =  SUBLISTC_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x1, x2, x3, x4)
APPEND1A_IN_AAG(x1, x2, x3)  =  APPEND1A_IN_AAG(x3)
U1_AAG(x1, x2, x3, x4, x5)  =  U1_AAG(x1, x4, x5)
U4_GG(x1, x2, x3, x4)  =  U4_GG(x1, x2, x3, x4)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x1, x2, x3, x4)
APPEND2B_IN_AGG(x1, x2, x3)  =  APPEND2B_IN_AGG(x2, x3)
U2_AGG(x1, x2, x3, x4, x5)  =  U2_AGG(x1, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 7 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPEND2B_IN_AGG(.(X1, X2), X3, .(X1, X4)) → APPEND2B_IN_AGG(X2, X3, X4)

The TRS R consists of the following rules:

append1cA_in_aag([], X1, X1) → append1cA_out_aag([], X1, X1)
append1cA_in_aag(.(X1, X2), X3, .(X1, X4)) → U7_aag(X1, X2, X3, X4, append1cA_in_aag(X2, X3, X4))
U7_aag(X1, X2, X3, X4, append1cA_out_aag(X2, X3, X4)) → append1cA_out_aag(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append1cA_in_aag(x1, x2, x3)  =  append1cA_in_aag(x3)
append1cA_out_aag(x1, x2, x3)  =  append1cA_out_aag(x1, x2, x3)
U7_aag(x1, x2, x3, x4, x5)  =  U7_aag(x1, x4, x5)
APPEND2B_IN_AGG(x1, x2, x3)  =  APPEND2B_IN_AGG(x2, x3)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPEND2B_IN_AGG(.(X1, X2), X3, .(X1, X4)) → APPEND2B_IN_AGG(X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPEND2B_IN_AGG(x1, x2, x3)  =  APPEND2B_IN_AGG(x2, x3)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPEND2B_IN_AGG(X3, .(X1, X4)) → APPEND2B_IN_AGG(X3, X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPEND2B_IN_AGG(X3, .(X1, X4)) → APPEND2B_IN_AGG(X3, X4)
    The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPEND1A_IN_AAG(.(X1, X2), X3, .(X1, X4)) → APPEND1A_IN_AAG(X2, X3, X4)

The TRS R consists of the following rules:

append1cA_in_aag([], X1, X1) → append1cA_out_aag([], X1, X1)
append1cA_in_aag(.(X1, X2), X3, .(X1, X4)) → U7_aag(X1, X2, X3, X4, append1cA_in_aag(X2, X3, X4))
U7_aag(X1, X2, X3, X4, append1cA_out_aag(X2, X3, X4)) → append1cA_out_aag(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append1cA_in_aag(x1, x2, x3)  =  append1cA_in_aag(x3)
append1cA_out_aag(x1, x2, x3)  =  append1cA_out_aag(x1, x2, x3)
U7_aag(x1, x2, x3, x4, x5)  =  U7_aag(x1, x4, x5)
APPEND1A_IN_AAG(x1, x2, x3)  =  APPEND1A_IN_AAG(x3)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPEND1A_IN_AAG(.(X1, X2), X3, .(X1, X4)) → APPEND1A_IN_AAG(X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPEND1A_IN_AAG(x1, x2, x3)  =  APPEND1A_IN_AAG(x3)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPEND1A_IN_AAG(.(X1, X4)) → APPEND1A_IN_AAG(X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPEND1A_IN_AAG(.(X1, X4)) → APPEND1A_IN_AAG(X4)
    The graph contains the following edges 1 > 1

(20) YES